T:Type, L:T List, P:(TProp). (xL. P(x))  (i:||L||. P(L[i])) 

latex

Definitions	xL. P(x), (x  l), P  Q, P  Q, x:A. B(x), A & B, , x(s), l[i], x:A. B(x), {i..j}, i  j < k, AB, P & Q, A, False, P  Q, ||as||, Prop, t  T
Lemmas	select wf, length wf1, int seg wf, nat wf, le wf